\begin{tabbing}
w{-}machine{-}independent($w$;$i$;$k$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let ${\it Choose}$,${\it Trans}$,${\it Send}$ = w{-}machine($w$;$i$) in \+
\\[0ex]$\forall$$s_{1}$, $s_{2}$:($x$:Id$\rightarrow\mathbb{Q}\rightarrow$vartype($i$;$x$)).
\\[0ex]($\forall$$z$:Id. ($\neg$($z$ = $x$)) $\Rightarrow$ ($s_{1}$($z$) = $s_{2}$($z$)))
\\[0ex]$\Rightarrow$ \=((\=$\forall$$v$:w{-}kindtype($w$.TA($i$);$w$.M;$i$)($k$).\+\+
\\[0ex]($\forall$$z$:Id. ($\neg$($z$ = $x$)) $\Rightarrow$ (${\it Trans}$($k$,$v$,$s_{1}$,$z$) = ${\it Trans}$($k$,$v$,$s_{2}$,$z$)))
\\[0ex]\& ${\it Send}$($k$,$v$,$\lambda$$x$.$s_{1}$($x$,0)) = ${\it Send}$($k$,$v$,$\lambda$$x$.$s_{2}$($x$,0)))
\-\\[0ex]\& (\=($\uparrow$islocal($k$))\+
\\[0ex]$\Rightarrow$ ($\forall$$n$:$\mathbb{N}$. ${\it Choose}$(act($k$),$n$,$\lambda$$x$.$s_{1}$($x$,0)) = ${\it Choose}$(act($k$),$n$,$\lambda$$x$.$s_{2}$($x$,0)))))
\-\-\-
\end{tabbing}